Concretise submonoid - #43611

PR summary 1201efd6e5

Import changes for modified files

No significant changes to the import graph

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

+AbsoluteValue.instCoeMonoidWithZeroHom
+MulEquiv.coe_toMonoidWithZeroHom
+MulEquiv.instCoeMonoidWithZeroHom
+OrderMonoidWithZeroHom.coe_coe
-OrderMonoidWithZeroHom.coe_comp_orderMonoidHom
-OrderMonoidWithZeroHom.coe_monoidWithZeroHom
-OrderMonoidWithZeroHom.coe_orderMonoidHom
+OrderMonoidWithZeroHom.coe_toMonoidWithZeroHom
+OrderMonoidWithZeroHom.coe_toOrderMonoidHom
+OrderMonoidWithZeroHom.instCoeMonoidWithZeroHom
-OrderMonoidWithZeroHom.mk_coe
+OrderMonoidWithZeroHom.mk_toMonoidWithZeroHom
-OrderMonoidWithZeroHom.ofClass_comp
-OrderMonoidWithZeroHom.ofClass_comp_monoidWithZeroHom
+OrderMonoidWithZeroHom.ofClass_eq_toMonoidWithZeroHom
-OrderMonoidWithZeroHom.ofClass_mk
+OrderMonoidWithZeroHom.toMonoidWithZeroHom_comp
-OrderMonoidWithZeroHom.toMonoidWithZeroHom_eq_ofClass
+OrderMonoidWithZeroHomClass.toOrderMonoidWithZeroHom.congr_simp
+RingHom.coe_toMonoidWithZeroHom
+RingHom.instCoeMonoidWithZeroHom
-RingHom.toMonoidWithZeroHom_eq_coe
+RingHom.toMonoidWithZeroHom_injective
-Valuation.IsEquiv.ofClass_eq_zero
+Valuation.IsRankOneDiscrete.instIsCyclicSubtypeUnitsMemSubgroupValueGroup
-Valuation.IsRankOneDiscrete.instIsCyclicSubtypeUnitsMemSubgroupValueGroupOfClass
-Valuation.OrderMonoidWithZeroHom.ofClass_monotone
-Valuation.coe_ofClass
+Valuation.coe_toMonoidWithZeroHom
+Valuation.instCoeMonoidWithZeroHom
+Valuation.instCommGroupWithZeroSubtypeMemSubmonoidMrange
-Valuation.instCommGroupWithZeroSubtypeMemSubmonoidMrangeMonoidWithZeroHomOfClass
+Valuation.instCommMonoidWithZeroSubtypeMemSubmonoidMrange
-Valuation.instCommMonoidWithZeroSubtypeMemSubmonoidMrangeMonoidWithZeroHomOfClass
-Valuation.instNontrivialSubtypeUnitsMemSubgroupValueGroupOfClassOfIsNontrivial
+Valuation.instNontrivialSubtypeUnitsMemSubgroupValueGroupOfIsNontrivial
-Valuation.instNontrivialSubtypeUnitsMemSubmonoidValueMonoidOfClassOfIsNontrivial
+Valuation.instNontrivialSubtypeUnitsMemSubmonoidValueMonoidOfIsNontrivial
-Valuation.map.congr_simp
+Valuation.map_comp
+Valuation.ofClass_eq_coe
-Valuation.toMonoidWithZeroHom_coe_eq_coe
-Valued.extensionValuation_coe_apply
+WithZero.coe_withZeroUnitsEquiv
-WithZero.ofClass_withZeroUnitsEquiv

No changes to strong technical debt.
No changes to weak technical debt.

Current commit 1201efd6e5
Reference commit a4bb538cf7

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.py pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

I believe some problems are caused by current partial change (still using FooHom.toMonoidHom, not uniformed to MonoidHomClass.toMonoidHom).

around half of problems can be solved by an additional MonoidHom.coe_coe.

I believe some problems are caused by current partial change (still using FooHom.toMonoidHom, not uniformed to MonoidHomClass.toMonoidHom).

That's very possible; I tried to do incremental changes. Do you have an example in mind which definitions (or lemmas) should be changed? Or do you mean that the fix should often be to use MonoidHomClass.toMonoidHom f instead of f.toMonoidHom (when f is e.g. an algebra morphism)? (I've certainly done this too often.)

That's very possible; I tried to do incremental changes. Do you have an example in mind which definitions (or lemmas) should be changed? Or do you mean that the fix should often be to use MonoidHomClass.toMonoidHom f instead of f.toMonoidHom (when f is e.g. an algebra morphism)? (I've certainly done this too often.)

It's more like choosing a normal form. Since instance synthesis don't see the two forms IsLocalization (M.map (MonoidHomClass.toMonoidHom f)) S and IsLocalization (M.map f.toMonoidHom) S are equal, we have to stick to one of them for the whole library. I believe the first one is what we want. Most of the theorems with hypothesis/conclusion including f.toMonoidHom should be changed to MonoidHomClass.toMonoidHom f.

I also did a minimal change to make mathlib build. Lots of f.toMonoidHom remains.

I accidentally pushed some changes related to removing coe to this PR.
Those changes should belong in a separate PR, split off from the definition modifications (this one). I'll handle the split later.

Opened #43765.

This pull request has conflicts, please merge master and resolve them.